Inference at * 
Iof proof for Lemma fast-fib:


  n:. {m:| m = fib(n)}  

latex

 by Assert n, a, b:.
 {m:| 
 {k:. (a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))}  

 {

latex

 1: .....assertion..... NILNIL

 1:   n, a, b:.
 1:   {m:| 
 1:   {k:.
 1:   {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))} 
 2: 

 2: 1. n, a, b:.
 2: 1. {m:| 
 2: 1. {k:.
 2: 1. {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))} 
 2:   n:. {m:| m = fib(n)} 
 .

Definitions

{x:A| B(x)} , x:A. B(x), A  B, P  Q, a < b, , n - m, #$n, s = t, , fib(n), n+m